Nuprl Lemma : filter_wf2
11,40
postcript
pdf
T
:Type,
l
:(
T
List),
P
:({
x
:
T
| (
x
l
)}
). filter(
P
;
l
)
({
x
:
T
| (
x
l
)} List)
latex
Definitions
filter(
P
;
l
)
,
(
x
l
)
,
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
list-subtype
,
bool
wf
,
l
member
wf
,
filter
wf
origin
T:Type, l:(T List), P:({x:T| (x 
l)} 
). filter(P;l) ({x:T| (x l)} List) T:Type, l:(T List), P:({x:T| (x l)} ). filter(P;l) ({x:T| (x l)} List) l)x:A. B(x) T